Add exact-scored O(3) tensor product benchmark - #12

Summary

• add an exact-scored O(3) irreducible-representation tensor-product benchmark runner
• add 12 self-contained easy/medium/hard sample problems in JSONL
• validate external dataset rows against a deterministic integer/parity oracle
• extract exactly one labelled FINAL ANSWER: line from PROOF.md
• add offline scorer, dataset-safety, prompt-leakage, and fake-OpenProver integration tests
• document list, sample-run, and external-dataset commands

Why

This is the first small contribution from the tensor-product decomposition benchmark series proposed in #11. It tests whether OpenProver can apply a supplied mathematical rule, justify the result, and emit an exact symbolic decomposition.

The task intentionally uses informal-proof mode rather than per-sample Lean equalities. Encoding each expected decomposition in a Lean theorem target would reveal the answer and reduce many samples to rfl or decide. The deterministic scorer remains the verification authority for this first version.

The bundled JSONL is only a reviewable sample. Larger benchmark datasets can be supplied with --dataset PATH and remain outside the OpenProver repository.

Scoring contract

For inputs l1 p1 and l2 p2, the oracle:

1. emits every degree from |l1-l2| through l1+l2;
2. multiplies parity with e*e=e, e*o=o, o*e=o, o*o=e;
3. requires ascending e3nn-style notation;
4. accepts exactly one FINAL ANSWER: marker from PROOF.md.

Wrong parity, order, missing/extra terms, duplicates, malformed syntax, missing markers, and ambiguous markers score zero.

Validation

• black --check scripts/run_irreps_tensor_product.py tests/test_irreps_tensor_product_benchmark.py
• ruff check scripts/run_irreps_tensor_product.py tests/test_irreps_tensor_product_benchmark.py
• pytest --ignore=tests/test_tui_keys.py -q — 32 passed
• python scripts/run_irreps_tensor_product.py --list
• git diff --check

The three excluded interactive TUI tests also fail unchanged on a clean upstream/master worktree: two require a real terminal stdin, and one still calls the removed max_steps setup argument.

Related to #11.